#LLM benchmark

3 篇

FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models

FormalTCS：评估 LLM 端到端理论计算机科学研究能力的基准

🧭 LLM 端到端科研能力评估

Harbin Institute of Technology

构建专家验证的 FormalTCS 基准，评估 LLM 在 STOC/FOCS/SODA/COLT 前沿 TCS 研究上的端到端能力，揭示自动形式化与科研品味是主要瓶颈。

📌 工作参考价值（3 点）

自动形式化是瓶颈：将自然语言需求转化为精确形式规范（如 SQL、DSL、策略规则）的能力远弱于在给定规范下的执行/证明能力。搭建 Agent 系统时，不要假设 LLM 能直接从模糊需求生成可执行逻辑，应设计中间表示或人工辅助的形式化步骤。
生成-过滤-证明流水线：采用“生成候选 → 自动过滤（规则/模型）→ 外部验证器（编译器、单元测试、仿真器）”的架构，将 LLM 生成和严格验证解耦，能显著提升最终输出质量。在推荐系统中，可用于自动生成策略规则、特征工程代码或查询重写规则，并用离线评估/在线 A/B 过滤。
评估基准设计：区分“给定形式化陈述的证明能力”与“从自然语言到形式化的转换能力”，避免用端到端指标掩盖子任务瓶颈。在业务中评估 LLM 能力时，应拆解为意图理解、结构化生成、逻辑推理等子任务分别评测。

Eval | 2026-08-20 | cs.CL | score 6/10

知识综合评审框架：多源证据综合LLM系统的任务级基准测试

🧭 LLM证据综合任务级评测与路由

Toronto Metropolitan University · Queen's University · Stellenbosch University

提出KSR人机协同框架，将证据综合拆解为筛选、抽取、分析、综合四任务并基准测评与路由，无单一系统全任务领先

📌 工作参考价值（4 点）

将复杂智能流程拆解为可独立评测的子任务（筛选/抽取/分析/综合），再按任务挑选最优模型或系统路由，可迁移到电商平台的商品评论分析、竞品报告生成、广告素材合规筛查等多源文档处理场景。
建立人工标注金标并报告 inter-rater reliability（如 Kappa=0.80）作为 LLM 效果上限参考，同时做数据污染检查，可避免模型评测被训练集泄漏或过度拟合金标误导。
多源异构信息（电商评论、社媒、政策、行业报告）的综合分析中，采用任务路由而非单一模型端到端生成，能暴露单源视角的盲点，例如论文发现 worker well-being、small firms、Global South 等跨源不对称问题，对市场洞察和风险识别有参考价值。
在业务中构建 LLM 驱动的知识管理或研究助手时，可借鉴其 human-in-the-loop 治理思路：将专家验证嵌入每个任务节点，保持流程透明可审计，降低模型在推理分析类任务上的不可控输出风险。

Eval | 2026-08-13 | cs.IR | score 6/10

AdvancedMathBench：高级数学证明生成与验证基准套件

🧭 数学推理基准与自动验证

Shanghai AI Laboratory · Shanghai Jiao Tong University · MMLab, The Chinese University of Hong Kong · Great Bay University

构建首个面向高级数学证明的生成-验证双任务基准，揭示前沿LLM在严谨推理上的严重瓶颈

📌 工作参考价值（3 点）

主要在数学推理领域有学术贡献，对电商、推荐、Agent等业务场景的可直接借鉴点有限。
自动验证管道的设计思路（结合细粒度错误判定与人类标注对齐）可迁移至任意需评估模型推理质量的场景，例如推荐解释生成的可信度自动评价、Agent规划步骤的正确性校验。
论文揭示的“错误检测能力弱”在推荐Agent中同样关键：当模型在长链任务中自行纠错时，细粒度判定逻辑可下沉为CoT过程的在线校验器。

Other | 2026-07-13 | HF Daily | score 6/10